Is the following a bug?  If not how do I get use an axiom ¬p to get
if p then a else b = b?
the proof BUG:

(DECL (P) |TRUTHVAL| CONSTANT)

(DECL (A B) |GROUND| CONSTANT)

(ASSUME |¬P|)
3. ¬P
   ctxt: (1)   deps: (3)

(TRW |IF P THEN A ELSE B| |*3*NIL|)
4. IF P THEN A ELSE B=IF P THEN A ELSE B
   ctxt: (1 2)   deps: (3)

(ASSUME |P|)
5. P
   ctxt: (1)   deps: (5)

(TRW |IF P THEN A ELSE B| |*5*NIL|)
6. IF P THEN A ELSE B=A
   ctxt: (1 2)   deps: (5)